Bernays–Schönfinkel class

The Bernays–Schönfinkel class (also known as Bernays–Schönfinkel-Ramsey class) of formulas, named after Paul Bernays and Moses Schönfinkel (and Frank P. Ramsey), is a decidable fragment of first-order logic formulas.

It is the set of satisfiable formulas which, when written in prenex normal form, have an $\exists^*\forall^*$ quantifier prefix and do not contain any function symbols.

This class of logic formulas is also sometimes referred as effectively propositional (EPR) since it can be effectively translated into propositional logic formulas by a process of grounding or instantiation.

References

Ramsey, F. (1930), "On a problem in formal logic", Proc. London Math. Soc. 30: 264–286, doi:10.1112/plms/s2-30.1.264
Piskac, R.; de Moura, L.; Bjorner, N. (December 2008), "Deciding Effectively Propositional Logic with Equality", Microsoft Research Technical Report (2008-181), http://research.microsoft.com/pubs/76532/tr-2008-181.pdf

‹The stub template below has been proposed for renaming to . See stub types for deletion to help reach a consensus on what to do.
Feel free to edit the template, but the template must not be blanked, and this notice must not be removed, until the discussion is closed. For more information, read the guide to deletion.›

Bernays–Schönfinkel class

See also

References